Skip to content
This repository has been archived by the owner on Jan 5, 2025. It is now read-only.

2.1章 running a program 修正 #21

Merged
merged 4 commits into from
May 27, 2024
Merged

2.1章 running a program 修正 #21

merged 4 commits into from
May 27, 2024

Conversation

imamuray
Copy link
Collaborator

@imamuray imamuray commented May 25, 2024

runnning-a-program.md に以下の修正を行いました。

  • 「IO アクションと呼ばれています」の文が重複していた箇所があったので削除しました。
  • 「IO アクション」の表記が「IO アクション」や「IOアクション」(IO後スペースなし)があったので「IO アクション」に統一しました。
  • ファイル中のほかの箇所で前後の半角スペースが入っていた単語に対し、前後の半角スペースを挿入しました。
    • 対象: RTS, バッククオートで囲まれた単語

runnning-a-program.md 以外も含むファイルに以下の修正を行いました。

  • 句読点直後にバッククオートで囲まれた単語がある場合に半角スペースが入っていた箇所の半角スペースを削除しました。

@s-taiga
Copy link
Contributor

s-taiga commented May 26, 2024

@imamuray
横から失礼します。
バッククォートで囲まれた文字列前後に半角スペースを追加する件について、句読点()の直後のものにスペースが入っていないように見受けられましたので、こちらも追加した方が良いように思いました。

Seasawher
Seasawher previously approved these changes May 26, 2024
@Seasawher
Copy link
Member

Seasawher commented May 26, 2024

ありがとうございます!
変更内容について問題ないと思います

@s-taiga

句読点(.と,)の直後のものにスペースが入っていないように見受けられましたので、

これについて、私がざっと差分を見た限りではどこが問題なのか分かりませんでした。具体的にどこなのかコードを引用していただけますか?

@imamuray
Copy link
Collaborator Author

imamuray commented May 26, 2024

句読点直後のバッククオートに半角スペースが入っているかについて私の方で調べてみました。
リポジトリ全体を , `|. ` の正規表現で検索かけたところ、現状だと2ヶ所のみ該当し、ほかの箇所にはないようでした(マークダウンの仕様上、正規表現の右側最後にスペース入ってしまっていますが検索時にはなしでやっています)。

該当箇所

アクセサドット記法は, 構造体のフィールド以外にも使えます. 任意の数の引数を取る関数にも使用できます. より一般的に,アクセサ記法は `TARGET.f ARG1 ARG2 ...` という形をしています.このとき `TARGET` の型が `T` であれば, `T.f` という関数が呼び出されます.`TARGET` は関数 `T.f` の型 `T` を持つ最初の引数になります. 多くの場合これは最初の引数ですが,常にではありません.`ARG1 ARG2 ...` は順に残りの引数として与えられます.例えば `String.append` は, `String``append` フィールドを持つ構造体ではないにもかかわらず,アクセサ記法を使って文字列から呼び出すことができます.

このとき TARGET の型が T であれば, T.f という

このプログラムでは,`main`アクションは`do`ブロックで構成されています.do ブロックには,一連の****(statement)が含まれています.それぞれの文は,`let` によるローカル変数の定義だったり,実行されるアクションであったりします.SQL がデータベースと対話するための特別な目的の言語と考えることができるように, `do` 構文は,Lean 内で命令型プログラムをモデル化するための専用のサブ言語だと考えることができます.`do` ブロックで構築された IO アクションは,文を順番に実行することで実行されます.

言語と考えることができるように, do 構文は

対応案

もし半角スペースを入れる方針とするなら、今まで訳されたファイルも対象としたほうがよいと考えます。その場合、変更が多くなるので PR は分けたほうがいいかもしれません。

半角スペースを入れない方針とするなら、変更箇所は2ヶ所なのでこの PR でやってしまってよいと考えます。

半角スペースを入れる/入れないどちらの対応の場合でも、README.md には半角スペースの入れ方について明記するとよいと考えました。

@s-taiga
Copy link
Contributor

s-taiga commented May 26, 2024

@Seasawher
言葉足らずですみません……imamurayさんが調査してくださった内容通りです。
@imamuray
ご調査ありがとうございます!
個人的には全角文字列と半角文字列の間には半角スペースを入れるというように決めた方がルール的にわかりやすいような気がしています。

@aconite-ac
Copy link
Contributor

aconite-ac commented May 26, 2024

修正ありがとうございます!

さて、ちょうど記号や記号前後の翻訳ルール(スタイルガイド)について提案しようと思っていたところでした。
原則として、スタイルガイドは第一に「読みやすい訳文を作る」ために、第二に「複数のスタイルがありうる場合に、訳者の選択コストを減らす」ために、スタイルを統一する目的で制定されるものと認識しています。
その上で、半角スペースに関する翻訳ルールについての自分の見解を述べさせていただきます。

日本語の文章において、文中で分かち書き(文中で語をスペースで区切る書き方)を行うことは少ないため、そもそも文中にスペースが入るスタイルは読者にとって読みにくいと考えています。
しかし、数学やプログラミングの文章においては、分かち書きを行うことで読みやすさが向上することの方が多いです。
これは英語が文中に登場することが多く、日本語と字幅の小さなアルファベットが隣接した際にスペースがないと著しく読みにくいからと考えています。
以下にTPiL4の和訳からの例を挙げます(ソース上ではなく文書上の表記を引用します):

言い換えれば、α から β への依存関数型は、インデックスが i と j の最大値である宇宙に「住んで」いる。

スペースが無いと次のようになります。

言い換えれば、αからβへの依存関数型は、インデックスがiとjの最大値である宇宙に「住んで」いる。

「iとj」の部分が非常に読みにくく感じたと思います。
この例のように、数学やプログラミングの文章において、(通常の文章と異なり例外的に)スペースを挟む一番の意義は、「字幅の小さなアルファベットに読みやすいだけの余白を提供する」ことにあると考えています。そして、字幅の小さな記号の後に半角スペースが足されると、文字間隔が大きくなりすぎて読みにくくなるように思えます。
この見解に基づき、「原則として全角文字列と半角文字列が隣接した場合は半角スペースを入れるが、(見た目の)字幅が小さな全角記号()の前後では半角スペースを入れない」というスタイルを提案いたします。

@aconite-ac
Copy link
Contributor

本題(2.1 の修正)についてですが、
原文では"IO action"という表記に統一されています。
また、この表記には「Lean のコードにおいて実際に IO という名前を用いる」というニュアンスが込められていると思われます。
("do block"という表記にもそのようなニュアンスが込められていると思います。)
したがって、訳文でも「IO アクション」という表記に統一するのが妥当だと思われます。

(返信や絵文字などで合意がいただけたらこちらでcommitを出して修正いたします。)

他の修正箇所については問題ないと思います。

@Seasawher
Copy link
Member

@aconite-ac 検討ありがとうございます!

「原則として全角文字列と半角文字列が隣接した場合は半角スペースを入れるが、(見た目の)字幅が小さな全角記号(、や。や・や:)の前後では半角スペースを入れない」

良いと思います。READMEに追記しておきます。

@imamuray
Copy link
Collaborator Author

imamuray commented May 26, 2024

@aconite-ac
返信ありがとうございます!

半角スペースの方針について私も問題ないと思います。

少し調べたところ、スペースの件やスタイルガイドをまとめていた記事を見つけたので貼っておきます。

linter があると目視確認の手間が省けるかもしれませんが、各自の環境でのセットアップの手間があるので一長一短あると思いました。

「IO アクション」の件についても原文を確認したところ、確かに「IO actions」と書かれていたので和訳も「IO アクション」で統一する方針でいいと思いました。
お手数をおかけしますが修正いただけると幸いです。

@imamuray
Copy link
Collaborator Author

@aconite-ac
先ほど修正お願いしましすと書きましたが、半角スペースが現状入っている2箇所の修正と合わせて IO アクションの修正も私がやろうと思います。

@aconite-ac
Copy link
Contributor

@imamuray
IO アクション」表記と半角スペース削除について修正commitを出していただきありがとうございます!
修正について問題ありませんので、他の方からの指摘もなさそうでしたら後ほどmergeいたします。

また、スタイルガイドとlinterに関するリンクも掲載していただきありがとうございます!
参考にさせていただきます。

@aconite-ac aconite-ac merged commit fe12332 into lean-ja:main May 27, 2024
2 checks passed
@imamuray imamuray deleted the 2.1-fix branch May 27, 2024 18:32
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants